A:Type, I:MaInterface(A), i:Id.
(i  ma-interface-locs(I))  (ma-interface-dom(I;i)  ({k:Knd| hasloc(k;i)}  List)) 

latex

Definitions	MaInterface(T), ma-interface-locs(I), ma-interface-dom(I;i), fpf-domain(f), t.2, x.A(x), t.1, t  T, f(x), left + right, Top, State(ds), {x:A| B(x)} , Knd, a:A fp B(a), Type, x. t(x), b, P  Q, P & Q, x:A  B(x), x:A. B(x), P  Q, P  Q, x:AB(x), (x  l), Id
Lemmas	member-fpf-dom, fpf-ap wf, pi1 wf, decl-state wf, fpf wf, pi2 wf, fpf-trivial-subtype-top, fpf-domain wf